${\it left}$ $\oplus$ ${\it right}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inl($\langle$${\it left}$$,\,$${\it right}$$\rangle$))